∂15-JAN-75  1448		1,DBX
 Thank you for your answer. I will come to your office Friday after
 the Representation seminar. Trying to prepare a draft or at least 
 a list of topics and send it to you earlier.
 
 Concernig the definition of value(e β):
 	What I wanted to say (but did in a confusing way) is, that a 
 distinction is needed between the function evaluating an expression
 (i.e. OPCONST value(EXPR)=VALUE in FOL notation with capitals for sorts)
 and the primitive functions which are used to define this function
 by giving values for the application of each binop.(i.e.
 OPCONST sum2(VALUE,VALUE)=VALUE, or 
 OPCONST apply(OPERATOR,VALUE,VALUE)=VALUE), or
 OPCONST valu(ISSUM)=VALUE, where
 	valu(mkesum(e1 e2))=sum2(value(e1),value(e2))
 (Sorry for using valu to distinct from val and value, it is in the
 style of your APpend !)
 It is possible to denote the function, which I have called sum2
 simply by the usual +, but an explanation is desirable, that in
 fact it is a metafunction, whose denotation happens to be
 identical to that of a concrete function symbol, which may
 occur in a concrete expression.